Inference at * 1 0 
Iof proof for Lemma absval zero:



1. i : 
  (if 0 z i then i else -i fi  = 0)  (i = 0) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{10:n,
 by PERMUTE{13:n,
 by PERMUTE{11:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{16:n,
 by PERMUTE{15:n,
 by PERMUTE{19:n} 

latex

 1: .....wf..... NILNIL

 1:   0 z i  
 2: .....wf..... NILNIL

 2:     Type
 3: .....wf..... NILNIL

 3: 2. 0 z i = tt
 3:   (0 z i = tt)  
 4: .....wf..... NILNIL

 4: 2. 0 z i = tt
 4:   (0 z i)  
 5: .....wf..... NILNIL

 5: 2. 0 z i = tt
 5:   (0  i)  
 6: .....wf..... NILNIL

 6: 2. 0 z i = tt
 6:   0 z i  
 7: .....wf..... NILNIL

 7: 2. 0 z i = tt
 7:   0  
 8: .....wf..... NILNIL

 8: 2. 0 z i = tt
 8:   i  
 9: 

 9: 2. 0  i
 9:   (if tt then i else -i fi  = 0)  (i = 0)
 10: .....wf..... NILNIL

 10: 2. 0 z i = ff
 10:   (0 z i = ff)  
 11: .....wf..... NILNIL

 11: 2. 0 z i = ff
 11:   (i <z 0)  
 12: .....wf..... NILNIL

 12: 2. 0 z i = ff
 12:   (i < 0)  
 13: .....wf..... NILNIL

 13: 2. 0 z i = ff
 13:   ((0 z i))  
 14: .....wf..... NILNIL

 14: 2. 0 z i = ff
 14:   0 z i  
 15: .....wf..... NILNIL

 15: 2. 0 z i = ff
 15:   0  
 16: .....wf..... NILNIL

 16: 2. 0 z i = ff
 16:   i  
 17: .....antecedent..... NILNIL

 17: 2. 0 z i = ff
 17:   True
 18: .....wf..... NILNIL

 18: 2. 0 z i = ff
 18: 3. ((0 z i)) = (i <z 0)
 18:    = 
 19: 

 19: 2. i < 0
 19:   (if ff then i else -i fi  = 0)  (i = 0)
 .

Definitions	{x:A| B(x)} , x.A(x), b, i <z j, a < b, ff, inr x , x:A  B(x), b, f(a), A  B, tt, , Ax, inl x , left + right, x:AB(x), Type, -n, #$n, i z j, if b then t else f fi , s = t, , , Unit, , True, T, P  Q, P & Q, P  Q, x:A. B(x), t  T, P  Q
Lemmas	assert of lt int, bnot of le int, bool wf, true wf, squash wf, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity